package contracts;

import java.util.Set;

import decorators.MoteurJeuDecorator;
import services.BombeService;
import services.MoteurJeuService;
import services.TerrainService;
import services.VilainService;
import utils.Commande;
import utils.Resultat;
import utils.Sante;

public class MoteurJeuContract extends MoteurJeuDecorator implements MoteurJeuService {

	public MoteurJeuContract(MoteurJeuService delegate){
		super(delegate);
	}

	public void checkInvariant() throws ContractException{
		/* [invariants]
	     		0 <= getPasJeuCourrant(M) <= getMaxPasJeu(M)
		 */
		int pas = getPasJeuCourrant();
		if(pas > getMaxPasJeu()){
			throw new InvariantException("Valeur de PasJeuCourant superieur strictement a maxPasJeu");
		}
		else if (pas < 0){
			throw new InvariantException("Valeur de PasJeuCourant strictement inferieur a 0");
		}

		/* 1 <= getHerosX() <= getTerrain().getNombreColonnes() */
		if(!(getHerosX() >= 1 && getHerosX() <= getTerrain().getNombreColonnes())){
			throw new InvariantException(
					"invariant 1 <= getHerosX() <= getTerrain().getNombreColonnes() non respectee");
		}

		/* 1 <= getHerosY() <= getTerrain().getNombreLignes() */
		if(!(getHerosY() >= 1 && getHerosY() <= getTerrain().getNombreLignes())){
			throw new InvariantException(
					"invariant 1 <= getHerosY() <= getTerrain().getNombreLignes() non respectee");
		}

		/* 3 <= getHerosForceVitale() <= 11 */
		if(!(getHerosForceVitale() >= 3 && getHerosForceVitale() <= 11)){
			throw new InvariantException(
					"invariant 3 <= getHerosForceVitale() <= 11 non respectee");
		}

		/* estFini() = (getHerosSante() = Sante.MORT || getPasJeuCourant() = getMaxPasJeu()) */
		if(!(estFini() == (getHerosSante() == Sante.MORT || getPasJeuCourrant() == getMaxPasJeu()))){
			throw new InvariantException(
					"invariant estFini() = (getHerosSante() = Sante.MORT || getPasJeuCourant() = getMaxPasJeu()) non respectee");
		}

		/* (resultatFinal() = Resultat.KIDNAPPEURGAGNE) = (getHerosSante() = Sante.MORT) */
		if(super.estFini()&&!((resultatFinal() == Resultat.KIDNAPPEURGAGNE) == (getHerosSante() == Sante.MORT))){
			throw new InvariantException(
					"invariant (resultatFinal() = Resultat.KIDNAPPEURGAGNE) = (getHerosSante() = Sante.MORT) non respectee");
		}

		/* (resultatFinal() = Resultat.PARTIENULLE) = (getHerosSante() = Sante.VIVANT) */
		if(super.estFini()&& !((resultatFinal() == Resultat.PARTIENULLE) == (getHerosSante() == Sante.VIVANT))){
			throw new InvariantException(
					"invariant (resultatFinal() = Resultat.PARTIENULLE) = (getHerosSante() = Sante.VIVANT) non respectee");
		}

		/* misEnJoue(x, y, num) = xB = getBombe(num).getX() && yB = getBombe(num).getY() &&
		 * aB = getBombe(num).getAmplitude() && 
		 * ((x=xB && Math.abs(y-yB) <= aB) || (y=yB && Math.abs(x-xB) <= aB))
		 */
		for(Integer num : this.getBombeNumeros()){
			BombeService s = this.getBombe(num);
			int x = this.getHerosX();
			int y = this.getHerosY();
			int xB = s.getX();
			int yB = s.getY();
			int aB = s.getAmplitude();
			if(!(misEnJoue(x, y, num) == ((x == xB && Math.abs(y - yB) <= aB) || (y == yB && Math.abs(x - xB) <= aB)))){
				throw new InvariantException("invariant misEnJoue non respectee");
			}
		}
	}

	@Override
	public int getMaxPasJeu() {
		return super.getMaxPasJeu();
	}

	@Override
	public int getPasJeuCourrant() {
		return super.getPasJeuCourrant();
	}

	@Override
	public int getHerosX(){
		return super.getHerosX();
	}

	@Override
	public int getHerosY(){
		return super.getHerosY();
	}

	@Override
	public int getKidnappeurX(){
		return super.getKidnappeurX();
	}

	@Override
	public int getKidnappeurY(){
		return super.getKidnappeurY();
	}

	@Override
	public Sante getHerosSante(){
		return super.getHerosSante();
	}

	@Override
	public Sante getKidnappeurSante(){
		return super.getKidnappeurSante();
	}

	@Override
	public int getHerosForceVitale(){
		return super.getHerosForceVitale();
	}

	@Override
	public int getForceVitaleKidnappeur(){
		return super.getForceVitaleKidnappeur();
	}

	@Override
	public TerrainService getTerrain(){
		return super.getTerrain();
	}

	@Override
	public Set<Integer> getBombeNumeros(){
		return super.getBombeNumeros();
	}

	@Override
	public int getNbBombes(){
		return super.getNbBombes();
	}

	@Override
	public int getNbVilains(){
		return super.getNbBombes();
	}

	@Override
	public Set<VilainService> getListeVilain(){
		return super.getListeVilain();
	}

	@Override
	public boolean bombeExiste(int num){
		return super.bombeExiste(num);
	}

	@Override
	public boolean vilainExiste(int num){
		return super.vilainExiste(num);
	}

	@Override
	public BombeService getBombe(int num) throws ContractException{
		if(!(bombeExiste(num))){
			throw new PreconditionException(
					"Precondition de getBombe non respectee");
		}
		return super.getBombe(num);
	}

	@Override
	public VilainService getVilain(int num) throws ContractException{
		if(!(vilainExiste(num))){
			throw new PreconditionException(
					"Precondition de getVilain non respectee");
		}
		return super.getVilain(num);
	}

	@Override
	public boolean estFini(){
		return super.estFini();
	}

	@Override
	public Resultat resultatFinal() throws ContractException{
		if(!(estFini())){
			System.out.println(estFini());
			throw new PreconditionException(
					"Precondition de resultatFinal non respectee");
		}
		return super.resultatFinal();
	}

	@Override
	public boolean misEnJoue(int x, int y, int num) throws ContractException{
		if(!(bombeExiste(num))){
			throw new PreconditionException(
					"Pr�condition de getBombe non respectee");
		}
		return super.misEnJoue(x, y, num);
	}

	@Override
	public void init(int maxPasJeu) throws ContractException {
		//\pre init(m) require m>= 0
		if(maxPasJeu < 0){
			throw new PreconditionException("maxPasJeu est inferieur a 0");
		}
		super.init(maxPasJeu);	
		this.checkInvariant();				

		//\post getMaxPasJeu(init(p)) = p
		if(maxPasJeu != getMaxPasJeu()){
			throw new PostconditionException("Postcondition sur maxPasJeu non valide : maxPasJeu different");
		}

		//\post getPasJeuCourrant(init(p)) = 0
		if(getPasJeuCourrant() !=0){
			throw new PostconditionException("Postcondition sur pasJeuCourant invalide : pasJeuCourant different de 0");
		}

		//\post getHerosX(init(p)) = 2
		if(getHerosX() != 2){
			throw new PostconditionException(
					"Postcondition de init sur getHerosX non respectee");
		}

		//\post getHerosY(init(p)) = 2
		if(getHerosY() != 2){
			throw new PostconditionException(
					"Postcondition de init sur getHerosY non respectee");
		}

		//\post getHerosSante(init(p)) = Sante.VIVANT
		if(getHerosSante() != Sante.VIVANT){
			throw new PostconditionException(
					"Postcondition de init sur getHerosSante non respectee");
		}

		//\post getHerosForceVitale(init(p)) = 3
		if(getHerosForceVitale() != 3){
			throw new PostconditionException(
					"Postcondition de init sur getHerosForceVitale non respectee");
		}

		//\post getTerrain().getNombreColonnes() = 15
		if(getTerrain().getNombreColonnes() != 15){
			throw new PostconditionException(
					"Postcondition de init sur getNombreColonnes non respectee");
		}

		//\post getTerrain().getNombreLignes() = 13
		if(getTerrain().getNombreLignes() != 13){
			throw new PostconditionException(
					"Postcondition de init sur getNombreLignes non respectee");
		}

		//\post getBombeNumeros(init(p)) = null
		if(getNbBombes() != 0){
			throw new PostconditionException(
					"Postcondition de init sur getBombeNumeros non respectee");
		}
	}

	@Override
	public void pasJeu(Commande c, boolean bool) throws ContractException{
		//\pre pasJeu(c) require !(estFini())
		if(estFini()){
			throw new PreconditionException("Precondition de pasJeu non respectee");
		}

		//ID bombe
		int numNextBombe = this.getBombeNumeros().size();
		
		//capture 
		int avPJC = this.getPasJeuCourrant();
		int avX = this.getHerosX();
		int avY = this.getHerosY();
		int avFV = this.getHerosForceVitale();
		TerrainService avT = this.getTerrain();
		super.pasJeu(c, bool);

		//\post getPasJeuCourant(pasJeu(c)) = getPasJeuCourant + 1
		if(!(this.getPasJeuCourrant() == avPJC + 1)){
			throw new PostconditionException("postcondition de pasJeu : getPasJeuCourant non respectee");
		}

		//\post getHerosX(pasJeu(Commande.GAUCHE)) = max(1, getHerosX() - 1)
		if(c == Commande.GAUCHE){
			if(!(this.getHerosX() == Math.max(1, avX - 1))){
				throw new PostconditionException("postcondition de pasJeu : getHerosX gauche non respectee");
			}
		}

		//\post getHerosX(pasJeu(Commande.DROITE)) = min(getTerrain().getNombreColonnes(), getHerosX() + 1)
		if(c == Commande.DROITE){
			if(!(this.getHerosX() == Math.min(this.getTerrain().getNombreColonnes(), avX + 1))){
				throw new PostconditionException("postcondition de pasJeu : getHerosX droite non respectee");
			}
		}

		//\post (c != Commande.GAUCHE && c != Commande.DROITE) => getHerosX(pasJeu(c)) = getHerosX()
		if(c != Commande.GAUCHE && c != Commande.DROITE){
			if(this.getHerosX() != avX){
				throw new PostconditionException("postcondition de pasJeu : getHerosX fixe non respectee");
			}
		}

		//\post getHerosY(pasJeu(Commande.HAUT)) = min(1, getHerosY() - 1)
		if(c == Commande.HAUT){
			if(!(this.getHerosY() == Math.min(1, avY - 1))){
				throw new PostconditionException("postcondition de pasJeu : getHerosY haut non respectee");
			}
		}

		//\post getHerosX(pasJeu(Commande.BAS)) = min(getTerrain().getNombreLignes(), getHerosY() + 1)
		if(c == Commande.BAS){
			if(!(this.getHerosY() == Math.min(this.getTerrain().getNombreLignes(), avY + 1))){
				throw new PostconditionException("postcondition de pasJeu : getHerosY bas non respectee");
			}
		}

		//\post (c != Commande.HAUT && c != Commande.BAS) => getHerosY(pasJeu(c)) = getHerosY()
		if(c != Commande.HAUT && c != Commande.BAS){
			if(this.getHerosY() != avY){
				throw new PostconditionException("postcondition de pasJeu : getHerosY fixe non respectee");
			}
		}

		//\post getHerosForceVitale(pasJeu(c)) == getHerosForceVitale()
		if(!(this.getHerosForceVitale() == avFV)){
			throw new PostconditionException("postcondition de pasJeu : getHerosForceVitale non respectee");
		}

		//\post getTerrain(pasJeu(c)) == getTerrain()
		if(!(this.getTerrain() == avT)){
			throw new PostconditionException("postcondition de pasJeu : getTerrain non respectee");
		}

		/*\post getBombeNumeros() \ num, 
		 * getBombe(pasJeu(Commande.BOMBE), num) = Bombe :init(num, getHerosX(), getHerosY(), getHerosForceVitale()) */
		if(c == Commande.BOMBE){
			if(!(this.getBombe(numNextBombe).getNumero() == numNextBombe
					&& this.getBombe(numNextBombe).getX() == this.getHerosX()
					&& this.getBombe(numNextBombe).getY() == this.getHerosY()
					&& this.getBombe(numNextBombe).getAmplitude() == this.getHerosForceVitale())){
				throw new PostconditionException("postcondition de pasJeu : getBombe non respectee");
			}
		}
	}

}
